perm filename DEMO[BMP,SYS]1 blob
sn#737807 filedate 1984-01-16 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00011 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 α⊃ to get THM
C00007 00003 (DEFN SUBEXP (X Y)
C00015 00004 (DEFN APPEND (U V) (IF (LISTP U) (CONS (CAR U) (APPEND (CDR U) V)) V))
C00021 00005 (DEFN REVERSE (U) (IF (LISTP U) (APPEND (REVERSE (CDR U)) (CONS (CAR U) NIL)) NIL))
C00033 00006 (DEFN SL (U V)
C00041 00007 (PROVE-LEMMA LENGTH-REVERSE (REWRITE)
C00047 00008 (DEFN FLATTEN (X)
C00051 00009 (ADD-SHELL ZN NIL ZNP
C00085 00010 (r '(REVERSE '(A B C)))
C00086 00011 (setq no-built-in-arith-flg t)
C00103 ENDMK
C⊗;
;;α⊃ to get THM
(BOOT-STRAP)
[ 4.088 0.0 ]
GROUND-ZERO
(MAKE-LIB "BOO")
(NOTE-LIB "BOO.LIB" "BOO.LISP")
(PROVE (IMPLIES (AND (NOT (LESSP X Z)) (LESSP Y Z)) (NOT (LESSP X Y)) ))
(PROVE (IMPLIES (AND (NOT (LESSP X Z)) (LESSP X Y)) (NOT (LESSP Y Z)) ))
(PROVE (IMPLIES (AND (LESSP X Y) (LESSP Y Z)) (LESSP X Z) ))
(DEFN SUBEXP (X Y)
(IF (LISTP Y)
(OR (EQUAL X Y) (SUBEXP X (CAR Y)) (SUBEXP X (CDR Y)))
(EQUAL X Y)) )
(PROVE (IMPLIES (AND (NOT (SUBEXP X Z)) (SUBEXP Y Z)) (NOT (SUBEXP X Y))) )
(PROVE (IMPLIES (AND (SUBEXP X Y) (SUBEXP Y Z)) (SUBEXP X Z) ))
(DEFN APPEND (U V) (IF (LISTP U) (CONS (CAR U) (APPEND (CDR U) V)) V))
(DEFN REVERSE (U) (IF (LISTP U) (APPEND (REVERSE (CDR U)) (CONS (CAR U) NIL)) NIL))
(DEFN PLISTP (X) (IF (LISTP X) (PLISTP (CDR X)) (EQUAL X NIL)))
(DEFN SL (U V)
(IF (AND (LISTP U)(LISTP V))
(SL (CDR U) (CDR V))
(AND (NOT (LISTP U)) (NOT (LISTP V))) ))
(PROVE-LEMMA ASSOCIATIVITY-OF-APPEND (REWRITE)
(EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))))
(PROVE-LEMMA APPEND-RIGHT-ID (REWRITE)
(IMPLIES (PLISTP X) (EQUAL (APPEND X NIL) X)))
(PROVE-LEMMA PLISTP-REVERSE (GENERALIZE REWRITE) (PLISTP (REVERSE X)))
(PROVE-LEMMA APPEND-REVERSE (REWRITE)
(EQUAL (REVERSE (APPEND A B)) (APPEND (REVERSE B) (REVERSE A))))
(PROVE-LEMMA REVERSE-REVERSE (REWRITE)
(IMPLIES (PLISTP X) (EQUAL (REVERSE (REVERSE X)) X)))
(DEFN APPEND (U V) (IF (LISTP U) (CONS (CAR U) (APPEND (CDR U) V)) V))
(DEFN REVERSE (U) (IF (LISTP U) (APPEND (REVERSE (CDR U)) (CONS (CAR U) NIL)) NIL))
(DEFN PLISTP (X) (IF (LISTP X) (PLISTP (CDR X)) (EQUAL X NIL)))
(DEFN SL (U V)
(IF (AND (LISTP U)(LISTP V))
(SL (CDR U) (CDR V))
(AND (NOT (LISTP U)) (NOT (LISTP V))) ))
(PROVE (SL U (REVERSE U)))
(PROVE-LEMMA LENGTH-REVERSE (REWRITE)
(EQUAL (LENGTH (REVERSE X)) (LENGTH X)))
(DEFN FLATTEN (X)
(IF (LISTP X) (APPEND (FLATTEN (CAR X)) (FLATTEN (CDR X))) (CONS X NIL)))
(DEFN MC-FLATTEN (X Y)
(IF (LISTP X) (MC-FLATTEN (CAR X) (MC-FLATTEN (CDR X) Y)) (CONS X Y)))
(PROVE-LEMMA FLATTEN-MC-FLATTEN (REWRITE)
(EQUAL (MC-FLATTEN X Y) (APPEND (FLATTEN X) Y)))
(DEFN SUBEXP (X Y)
(IF (LISTP Y)
(OR (EQUAL X Y) (SUBEXP X (CAR Y)) (SUBEXP X (CDR Y)))
(EQUAL X Y)) )
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP can be
used to prove that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each recursive call. Hence, SUBEXP is
accepted under the principle of definition. Observe that:
(OR (FALSEP (SUBEXP X Y))
(TRUEP (SUBEXP X Y)))
is a theorem.
[ 1.50100009 0.069999949 ]
SUBEXP
(PROVE '(IMPLIES (AND (NOT (SUBEXP X Z)) (SUBEXP Y Z)) (NOT (SUBEXP X Y))) )
Name the conjecture *1.
We will try to prove it by induction. Three inductions are
suggested by terms in the conjecture. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP Z)
(P X Y (CAR Z))
(P X Y (CDR Z)))
(P X Y Z))
(IMPLIES (NOT (LISTP Z)) (P X Y Z))).
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP can be used
to prove that the measure (COUNT Z) decreases according to the
well-founded relation LESSP in each induction step of the scheme.
The above induction scheme produces five new formulas:
Case 5. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CAR Z))
(SUBEXP X (CDR Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, opening up the definition of SUBEXP, to:
T.
Case 4. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CAR Z)))
(SUBEXP X (CDR Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))),
which we simplify, opening up SUBEXP, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CAR Z))
(NOT (SUBEXP Y (CDR Z)))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))),
which we simplify, unfolding SUBEXP, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CAR Z)))
(NOT (SUBEXP Y (CDR Z)))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, opening up SUBEXP, to:
(IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CAR Z)))
(NOT (SUBEXP Y (CDR Z)))
(NOT (EQUAL X Z))
(NOT (SUBEXP X (CAR Z)))
(NOT (SUBEXP X (CDR Z)))
(EQUAL Y Z))
(NOT (SUBEXP X Y))),
which we again simplify, unfolding the function SUBEXP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))),
which we simplify, expanding the definition of SUBEXP, to:
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL X Z))
(EQUAL Y Z))
(NOT (EQUAL X Y))),
which we again simplify, obviously, to:
T.
That finishes the proof of *1. Q.E.D.
PROVED
(PROVE-LEMMA TRANSITIVITY-OF-SUBEXP NIL
(IMPLIES (AND (SUBEXP X Y) (SUBEXP Y Z)) (SUBEXP X Z) ))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms
in the conjecture suggest three inductions. They merge into two
likely candidate inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Z)
(P X (CAR Z) Y)
(P X (CDR Z) Y))
(P X Z Y))
(IMPLIES (NOT (LISTP Z)) (P X Z Y))).
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP inform us
that the measure (COUNT Z) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above
induction scheme generates five new conjectures:
Case 5. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CAR Z)))
(NOT (SUBEXP Y (CDR Z)))
(SUBEXP X Y)
(SUBEXP Y Z))
(SUBEXP X Z)),
which simplifies, opening up the definition of SUBEXP, to:
T.
Case 4. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CAR Z))
(NOT (SUBEXP Y (CDR Z)))
(SUBEXP X Y)
(SUBEXP Y Z))
(SUBEXP X Z)).
This simplifies, expanding the function SUBEXP, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CAR Z)))
(SUBEXP X (CDR Z))
(SUBEXP X Y)
(SUBEXP Y Z))
(SUBEXP X Z)),
which we simplify, expanding the function SUBEXP, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CAR Z))
(SUBEXP X (CDR Z))
(SUBEXP X Y)
(SUBEXP Y Z))
(SUBEXP X Z)).
This simplifies, opening up SUBEXP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Z))
(SUBEXP X Y)
(SUBEXP Y Z))
(SUBEXP X Z)),
which simplifies, opening up the function SUBEXP, to:
(IMPLIES (AND (NOT (LISTP Z))
(SUBEXP X Y)
(EQUAL Y Z))
(EQUAL X Y)).
However this simplifies again, unfolding the function SUBEXP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.62700005 0.32599996 ]
TRANSITIVITY-OF-SUBEXP
(DEFN APPEND (U V) (IF (LISTP U) (CONS (CAR U) (APPEND (CDR U) V)) V))
Linear arithmetic and the lemma CDR-LESSP inform us that the
measure (COUNT U) decreases according to the well-founded relation
LESSP in each recursive call. Hence, APPEND is accepted under the
principle of definition. Observe that:
(OR (LISTP (APPEND U V))
(EQUAL (APPEND U V) V))
is a theorem.
[ 0.18600006 0.05600001 ]
APPEND
(DEFN PLISTP (X) (IF (LISTP X) (PLISTP (CDR X)) (EQUAL X NIL)))
Linear arithmetic and the lemma CDR-LESSP establish that the
measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call. Hence, PLISTP is accepted under the
principle of definition. Observe that:
(OR (FALSEP (PLISTP X))
(TRUEP (PLISTP X)))
is a theorem.
[ 0.307999928 0.055000051 ]
PLISTP
(PROVE-LEMMA ASSOCIATIVITY-OF-APPEND (REWRITE)
(EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms
in the conjecture suggest three inductions. They merge into two
likely candidate inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X) (P (CDR X) Y Z))
(P X Y Z))
(IMPLIES (NOT (LISTP X)) (P X Y Z))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) (APPEND Y Z))))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
unfolding APPEND, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, expanding the definition of APPEND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.505999885 0.203000132 ]
ASSOCIATIVITY-OF-APPEND
(PROVE-LEMMA APPEND-RIGHT-ID (REWRITE)
(IMPLIES (PLISTP X) (EQUAL (APPEND X NIL) X)))
Call the conjecture *1.
Perhaps we can prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X) (P (CDR X)))
(P X))
(IMPLIES (NOT (LISTP X)) (P X))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
produces three new formulas:
Case 3. (IMPLIES (AND (LISTP X)
(NOT (PLISTP (CDR X)))
(PLISTP X))
(EQUAL (APPEND X NIL) X)).
This simplifies, expanding the definition of PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (APPEND (CDR X) NIL) (CDR X))
(PLISTP X))
(EQUAL (APPEND X NIL) X)),
which simplifies, applying the lemma CONS-CAR-CDR, and unfolding
PLISTP and APPEND, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X)) (PLISTP X))
(EQUAL (APPEND X NIL) X)),
which simplifies, expanding the definitions of PLISTP, APPEND, and
EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.316999815 0.215000153 ]
APPEND-RIGHT-ID
(DEFN REVERSE (U) (IF (LISTP U) (APPEND (REVERSE (CDR U)) (CONS (CAR U) NIL)) NIL))
Linear arithmetic and the lemma CDR-LESSP inform us that the
measure (COUNT U) decreases according to the well-founded relation
LESSP in each recursive call. Hence, REVERSE is accepted under the
definitional principle. Note that:
(OR (LITATOM (REVERSE U))
(LISTP (REVERSE U)))
is a theorem.
[ 0.078000005 0.0540000917 ]
REVERSE
(PROVE-LEMMA PLISTP-REVERSE (GENERALIZE REWRITE) (PLISTP (REVERSE X)))
Give the conjecture the name *1.
Let us appeal to the induction principle. There is only one
suggested induction. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP X) (P (CDR X)))
(P X))
(IMPLIES (NOT (LISTP X)) (P X))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP X)
(PLISTP (REVERSE (CDR X))))
(PLISTP (REVERSE X))),
which simplifies, opening up the definition of REVERSE, to:
(IMPLIES (AND (LISTP X)
(PLISTP (REVERSE (CDR X))))
(PLISTP (APPEND (REVERSE (CDR X))
(LIST (CAR X))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z)
to eliminate (CDR X) and (CAR X). This generates:
(IMPLIES (PLISTP (REVERSE Z))
(PLISTP (APPEND (REVERSE Z) (LIST V)))),
which we generalize by replacing (REVERSE Z) by Y. We would thus
like to prove the formula:
(IMPLIES (PLISTP Y)
(PLISTP (APPEND Y (LIST V)))),
which we will name *1.1.
Case 1. (IMPLIES (NOT (LISTP X))
(PLISTP (REVERSE X))).
This simplifies, opening up the functions REVERSE and PLISTP, to:
T.
So next consider:
(IMPLIES (PLISTP Y)
(PLISTP (APPEND Y (LIST V)))),
which is formula *1.1 above. Perhaps we can prove it by induction.
The recursive terms in the conjecture suggest two inductions.
However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (P (CDR Y) V))
(P Y V))
(IMPLIES (NOT (LISTP Y)) (P Y V))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads
to three new formulas:
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (PLISTP (CDR Y)))
(PLISTP Y))
(PLISTP (APPEND Y (LIST V)))),
which simplifies, expanding the definition of PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(PLISTP (APPEND (CDR Y) (LIST V)))
(PLISTP Y))
(PLISTP (APPEND Y (LIST V)))),
which we simplify, rewriting with CDR-CONS, and unfolding the
definitions of PLISTP and APPEND, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y)) (PLISTP Y))
(PLISTP (APPEND Y (LIST V)))).
This simplifies, applying CDR-CONS, and expanding the functions
PLISTP, LISTP, and APPEND, to:
T.
That finishes the proof of *1.1, which finishes the proof of *1.
Q.E.D.
[ 0.62700005 0.464000065 ]
PLISTP-REVERSE
(PROVE-LEMMA APPEND-REVERSE (REWRITE)
(EQUAL (REVERSE (APPEND A B)) (APPEND (REVERSE B) (REVERSE A))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms
in the conjecture suggest three inductions. They merge into two
likely candidate inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (P (CDR A) B))
(P A B))
(IMPLIES (NOT (LISTP A)) (P A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP A)
(EQUAL (REVERSE (APPEND (CDR A) B))
(APPEND (REVERSE B)
(REVERSE (CDR A)))))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B) (REVERSE A)))),
which simplifies, applying the lemmas CAR-CONS and CDR-CONS, and
unfolding APPEND and REVERSE, to:
(IMPLIES (AND (LISTP A)
(EQUAL (REVERSE (APPEND (CDR A) B))
(APPEND (REVERSE B)
(REVERSE (CDR A)))))
(EQUAL (APPEND (REVERSE (APPEND (CDR A) B))
(LIST (CAR A)))
(APPEND (REVERSE B)
(APPEND (REVERSE (CDR A))
(LIST (CAR A)))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace A by (CONS Z X)
to eliminate (CDR A) and (CAR A). We would thus like to prove:
(IMPLIES (EQUAL (REVERSE (APPEND X B))
(APPEND (REVERSE B) (REVERSE X)))
(EQUAL (APPEND (REVERSE (APPEND X B))
(LIST Z))
(APPEND (REVERSE B)
(APPEND (REVERSE X) (LIST Z))))).
We use the above equality hypothesis by substituting:
(APPEND (REVERSE B) (REVERSE X))
for (REVERSE (APPEND X B)) and throwing away the equality. We must
thus prove:
(EQUAL (APPEND (APPEND (REVERSE B) (REVERSE X))
(LIST Z))
(APPEND (REVERSE B)
(APPEND (REVERSE X) (LIST Z)))),
which further simplifies, rewriting with ASSOCIATIVITY-OF-APPEND,
to:
T.
Case 1. (IMPLIES (NOT (LISTP A))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B) (REVERSE A)))).
This simplifies, rewriting with the lemmas PLISTP-REVERSE and
APPEND-RIGHT-ID, and expanding APPEND and REVERSE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.22599997 0.35400009 ]
APPEND-REVERSE
(PROVE-LEMMA REVERSE-REVERSE (REWRITE)
(IMPLIES (PLISTP X) (EQUAL (REVERSE (REVERSE X)) X)))
Give the conjecture the name *1.
We will try to prove it by induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP X) (P (CDR X)))
(P X))
(IMPLIES (NOT (LISTP X)) (P X))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads
to the following three new goals:
Case 3. (IMPLIES (AND (LISTP X)
(NOT (PLISTP (CDR X)))
(PLISTP X))
(EQUAL (REVERSE (REVERSE X)) X)),
which we simplify, expanding PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (REVERSE (REVERSE (CDR X)))
(CDR X))
(PLISTP X))
(EQUAL (REVERSE (REVERSE X)) X)).
This simplifies, applying CAR-CONS, CDR-CONS, CONS-CAR-CDR, and
APPEND-REVERSE, and unfolding PLISTP, REVERSE, APPEND, and LISTP,
to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X)) (PLISTP X))
(EQUAL (REVERSE (REVERSE X)) X)),
which simplifies, expanding the definitions of PLISTP, REVERSE, and
EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.265999857 0.228000132 ]
REVERSE-REVERSE
(DEFN SL (U V)
(IF (AND (LISTP U)(LISTP V))
(SL (CDR U) (CDR V))
(AND (NOT (LISTP U)) (NOT (LISTP V))) ))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of AND establish that the measure (COUNT U) decreases
according to the well-founded relation LESSP in each recursive call.
Hence, SL is accepted under the definitional principle. The
definition of SL can be justified in another way. Linear arithmetic,
the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of AND can
be used to establish that the measure (COUNT V) decreases according
to the well-founded relation LESSP in each recursive call. Note that:
(OR (FALSEP (SL U V))
(TRUEP (SL U V)))
is a theorem.
[ 0.82200012 0.109999848 ]
SL
(PROVE '(SL U (REVERSE U)))
Call the conjecture *1.
Perhaps we can prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (AND (AND (LISTP U) (LISTP (REVERSE U)))
(P (CDR U)))
(P U))
(IMPLIES (NOT (AND (LISTP U) (LISTP (REVERSE U))))
(P U))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of AND establish that the measure (COUNT U) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
two new formulas:
Case 2. (IMPLIES (AND (AND (LISTP U) (LISTP (REVERSE U)))
(SL (CDR U) (REVERSE (CDR U))))
(SL U (REVERSE U))).
This simplifies, expanding REVERSE and AND, to:
(IMPLIES (AND (LISTP U)
(SL (CDR U) (REVERSE (CDR U))))
(SL U
(APPEND (REVERSE (CDR U))
(LIST (CAR U))))).
Applying the lemma CAR-CDR-ELIM, replace U by (CONS Z X) to
eliminate (CDR U) and (CAR U). We would thus like to prove:
(IMPLIES (SL X (REVERSE X))
(SL (CONS Z X)
(APPEND (REVERSE X) (LIST Z)))),
which we further simplify, rewriting with CDR-CONS, and unfolding
the function SL, to:
(IMPLIES (SL X (REVERSE X))
(SL X
(CDR (APPEND (REVERSE X) (LIST Z))))),
which we generalize by replacing (REVERSE X) by Y. We restrict the
new variable by recalling PLISTP-REVERSE. This generates the new
conjecture:
(IMPLIES (AND (PLISTP Y) (SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))),
which we will name *1.1.
Case 1. (IMPLIES (NOT (AND (LISTP U) (LISTP (REVERSE U))))
(SL U (REVERSE U))),
which we simplify, opening up REVERSE, AND, LISTP, and SL, to:
T.
So let us turn our attention to:
(IMPLIES (AND (PLISTP Y) (SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))),
which we named *1.1 above. Let us appeal to the induction principle.
Five inductions are suggested by terms in the conjecture. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (P (CDR X) (CDR Y) Z))
(P X Y Z))
(IMPLIES (NOT (LISTP Y)) (P X Y Z))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive
instance chosen for X. The above induction scheme leads to four new
formulas:
Case 4. (IMPLIES (AND (LISTP Y)
(NOT (PLISTP (CDR Y)))
(PLISTP Y)
(SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))),
which simplifies, unfolding the definition of PLISTP, to:
T.
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (SL (CDR X) (CDR Y)))
(PLISTP Y)
(SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))).
This simplifies, unfolding the definitions of PLISTP and SL, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(SL (CDR X)
(CDR (APPEND (CDR Y) (LIST Z))))
(PLISTP Y)
(SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))),
which we simplify, rewriting with CDR-CONS, and expanding the
functions PLISTP, SL, and APPEND, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y))
(PLISTP Y)
(SL X Y))
(SL X (CDR (APPEND Y (LIST Z))))).
This simplifies, rewriting with CDR-CONS, and opening up PLISTP,
LISTP, SL, and APPEND, to:
T.
That finishes the proof of *1.1, which, consequently, also
finishes the proof of *1. Q.E.D.
PROVED
(PROVE-LEMMA LENGTH-REVERSE (REWRITE)
(EQUAL (LENGTH (REVERSE X)) (LENGTH X)))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest two inductions. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP X) (P (CDR X)))
(P X))
(IMPLIES (NOT (LISTP X)) (P X))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
produces two new formulas:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (LENGTH (REVERSE (CDR X)))
(LENGTH (CDR X))))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))).
This simplifies, opening up the definitions of REVERSE and LENGTH,
to:
(IMPLIES (AND (LISTP X)
(EQUAL (LENGTH (REVERSE (CDR X)))
(LENGTH (CDR X))))
(EQUAL (LENGTH (APPEND (REVERSE (CDR X))
(LIST (CAR X))))
(ADD1 (LENGTH (CDR X))))).
Applying the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to
eliminate (CDR X) and (CAR X). We must thus prove:
(IMPLIES (EQUAL (LENGTH (REVERSE Z))
(LENGTH Z))
(EQUAL (LENGTH (APPEND (REVERSE Z) (LIST V)))
(ADD1 (LENGTH Z)))).
We use the above equality hypothesis by substituting
(LENGTH (REVERSE Z)) for (LENGTH Z) and throwing away the equality.
We must thus prove:
(EQUAL (LENGTH (APPEND (REVERSE Z) (LIST V)))
(ADD1 (LENGTH (REVERSE Z)))).
We will try to prove the above conjecture by generalizing it,
replacing (REVERSE Z) by Y. We restrict the new variable by
recalling PLISTP-REVERSE. This produces:
(IMPLIES (PLISTP Y)
(EQUAL (LENGTH (APPEND Y (LIST V)))
(ADD1 (LENGTH Y)))),
which we will name *1.1.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))),
which we simplify, opening up REVERSE, LENGTH, and EQUAL, to:
T.
So let us turn our attention to:
(IMPLIES (PLISTP Y)
(EQUAL (LENGTH (APPEND Y (LIST V)))
(ADD1 (LENGTH Y)))),
which we named *1.1 above. Let us appeal to the induction principle.
Three inductions are suggested by terms in the conjecture. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (P (CDR Y) V))
(P Y V))
(IMPLIES (NOT (LISTP Y)) (P Y V))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads
to three new formulas:
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (PLISTP (CDR Y)))
(PLISTP Y))
(EQUAL (LENGTH (APPEND Y (LIST V)))
(ADD1 (LENGTH Y)))),
which simplifies, unfolding the definition of PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(EQUAL (LENGTH (APPEND (CDR Y) (LIST V)))
(ADD1 (LENGTH (CDR Y))))
(PLISTP Y))
(EQUAL (LENGTH (APPEND Y (LIST V)))
(ADD1 (LENGTH Y)))).
This simplifies, rewriting with CDR-CONS, and expanding the
functions PLISTP, APPEND, and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y)) (PLISTP Y))
(EQUAL (LENGTH (APPEND Y (LIST V)))
(ADD1 (LENGTH Y)))),
which simplifies, applying CDR-CONS, and opening up the definitions
of PLISTP, LISTP, APPEND, ADD1, LENGTH, and EQUAL, to:
T.
That finishes the proof of *1.1, which also finishes the proof
of *1. Q.E.D.
[ 1.85900015 0.584999844 ]
LENGTH-REVERSE
(DEFN FLATTEN (X)
(IF (LISTP X) (APPEND (FLATTEN (CAR X)) (FLATTEN (CDR X))) (CONS X NIL)))
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP inform
us that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each recursive call. Hence, FLATTEN is accepted
under the principle of definition. From the definition we can
conclude that (LISTP (FLATTEN X)) is a theorem.
[ 0.109999848 0.055000051 ]
FLATTEN
(DEFN MC-FLATTEN (X Y)
(IF (LISTP X) (MC-FLATTEN (CAR X) (MC-FLATTEN (CDR X) Y)) (CONS X Y)))
Linear arithmetic and the lemmas CAR-LESSP and CDR-LESSP inform
us that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MC-FLATTEN is accepted
under the principle of definition. From the definition we can
conclude that (LISTP (MC-FLATTEN X Y)) is a theorem.
[ 0.107999929 0.055000051 ]
MC-FLATTEN
(PROVE-LEMMA FLATTEN-MC-FLATTEN (REWRITE)
(EQUAL (MC-FLATTEN X Y) (APPEND (FLATTEN X) Y)))
Call the conjecture *1.
Perhaps we can prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X)
(P (CAR X) (MC-FLATTEN (CDR X) Y))
(P (CDR X) Y))
(P X Y))
(IMPLIES (NOT (LISTP X)) (P X Y))).
Linear arithmetic and the lemmas CAR-LESSP and CDR-LESSP establish
that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each induction step of the scheme. Note, however,
the inductive instances chosen for Y. The above induction scheme
produces two new formulas:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (MC-FLATTEN (CAR X)
(MC-FLATTEN (CDR X) Y))
(APPEND (FLATTEN (CAR X))
(MC-FLATTEN (CDR X) Y)))
(EQUAL (MC-FLATTEN (CDR X) Y)
(APPEND (FLATTEN (CDR X)) Y)))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X) Y))).
This simplifies, applying ASSOCIATIVITY-OF-APPEND, and expanding
MC-FLATTEN and FLATTEN, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X) Y))).
This simplifies, applying CDR-CONS and CAR-CONS, and unfolding
MC-FLATTEN, FLATTEN, APPEND, and LISTP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.247000122 0.22400004 ]
FLATTEN-MC-FLATTEN
(ADD-SHELL ZN NIL ZNP
((POS (ONE-OF NUMBERP) ZERO) (NEG (ONE-OF NUMBERP) ZERO)))
[ 0.70500005 0.0 ]
ZN
(DEFN ZLESSP (X Y)
(LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))
Note that (OR (FALSEP (ZLESSP X Y)) (TRUEP (ZLESSP X Y))) is a
theorem.
[ 0.279000092 0.0149998983 ]
ZLESSP
(DEFN ZLESSEQP (X Y) (NOT (ZLESSP Y X)))
Note that (OR (FALSEP (ZLESSEQP X Y)) (TRUEP (ZLESSEQP X Y))) is
a theorem.
[ 0.0310000102 0.0149998983 ]
ZLESSEQP
(DEFN ZMAX (X Y) (IF (ZLESSP X Y) Y X))
Observe that (OR F (EQUAL (ZMAX X Y) X) (EQUAL (ZMAX X Y) Y)) is
a theorem.
[ 0.0280001322 0.016999817 ]
ZMAX
(DEFN ZMIN (X Y) (IF (ZLESSP X Y) X Y))
Observe that (OR F (EQUAL (ZMIN X Y) X) (EQUAL (ZMIN X Y) Y)) is
a theorem.
[ 0.0289998373 0.0160001118 ]
ZMIN
(DEFN ZSUB1 (X) (ZN (POS X) (ADD1 (NEG X))))
Note that (ZNP (ZSUB1 X)) is a theorem.
[ 0.0299997965 0.0110000611 ]
ZSUB1
(DEFN PZDIFFERENCE (X Y)
(DIFFERENCE (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))
Note that (NUMBERP (PZDIFFERENCE X Y)) is a theorem.
[ 0.24900004 0.0120000204 ]
PZDIFFERENCE
(DEFN M1 (X Y Z) (IF (ZLESSEQP X Y) 0 1))
WARNING: Z is in the arglist but not in the body of the definition
of M1!
Note that (NUMBERP (M1 X Y Z)) is a theorem.
[ 0.0489997864 0.0110000611 ]
M1
(DEFN M2 (X Y Z) (PZDIFFERENCE (ZMAX X (ZMAX Y Z)) (ZMIN X (ZMIN Y Z))))
Note that (NUMBERP (M2 X Y Z)) is a theorem.
[ 0.0460001626 0.011999766 ]
M2
(DEFN M3 (X Y Z) (PZDIFFERENCE X (ZMIN X (ZMIN Y Z))))
From the definition we can conclude that (NUMBERP (M3 X Y Z)) is
a theorem.
[ 0.033999888 0.0150001526 ]
M3
(DEFN TAK0 (X Y Z) (IF (ZLESSEQP X Y) Y (IF (ZLESSEQP Y Z) Z X)))
From the definition we can conclude that:
(OR F
(EQUAL (TAK0 X Y Z) X)
(EQUAL (TAK0 X Y Z) Y)
(EQUAL (TAK0 X Y Z) Z))
is a theorem.
[ 0.0409998577 0.0280001322 ]
TAK0
(DEFN M (X Y Z) (CONS (M1 X Y Z) (CONS (M2 X Y Z) (CONS (M3 X Y Z) NIL))))
Note that (LISTP (M X Y Z)) is a theorem.
[ 0.052999878 0.0110000611 ]
M
(PROVE-LEMMA TAK0-SATISFIES-TAK-EQUATION NIL
(EQUAL (TAK0 X Y Z)
(IF (ZLESSEQP X Y) Y
(TAK0 (TAK0 (ZSUB1 X) Y Z)
(TAK0 (ZSUB1 Y) Z X)
(TAK0 (ZSUB1 Z) X Y)))))
This conjecture simplifies, rewriting with the lemmas POS-ZN and
NEG-ZN, and unfolding the functions ZLESSEQP, ZLESSP, TAK0, and ZSUB1,
to 24 new conjectures:
Case 24.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Z X
(ZN (POS Z) (ADD1 (NEG Z)))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 23.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
X
(ZN (POS Z) (ADD1 (NEG Z)))))),
which we again simplify, using linear arithmetic, to:
T.
Case 22.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 Y X
(ZN (POS Z) (ADD1 (NEG Z)))))).
However this simplifies again, using linear arithmetic, to:
T.
Case 21.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Y X
(ZN (POS Z) (ADD1 (NEG Z)))))).
This simplifies again, using linear arithmetic, to:
T.
Case 20.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Z
(ZN (POS Y) (ADD1 (NEG Y)))
(ZN (POS Z) (ADD1 (NEG Z)))))),
which we again simplify, using linear arithmetic, to:
T.
Case 19.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
(ZN (POS Y) (ADD1 (NEG Y)))
(ZN (POS Z) (ADD1 (NEG Z)))))).
However this simplifies again, using linear arithmetic, to:
T.
Case 18.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 Y
(ZN (POS Y) (ADD1 (NEG Y)))
(ZN (POS Z) (ADD1 (NEG Z)))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 17.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Y
(ZN (POS Y) (ADD1 (NEG Y)))
(ZN (POS Z) (ADD1 (NEG Z)))))).
But this simplifies again, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Z Z
(ZN (POS Z) (ADD1 (NEG Z)))))).
However this simplifies again, rewriting with SUB1-ADD1, NEG-ZN,
and POS-ZN, and opening up LESSP, PLUS, ZLESSEQP, ZLESSP, and TAK0,
to:
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y)))
(LESSP (PLUS (POS Z) (NEG Z))
(PLUS (NEG Z) (POS Z)))
(NOT (EQUAL (PLUS (POS Z) (NEG Z)) 0))
( LEQ
(PLUS (NEG Z) (POS Z))
(SUB1 (PLUS (POS Z) (NEG Z)))))
(EQUAL Z
(ZN (POS Z) (ADD1 (NEG Z))))).
This simplifies again, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
Z
(ZN (POS Z) (ADD1 (NEG Z)))))),
which we again simplify, using linear arithmetic, to:
T.
Case 14.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 Y Z
(ZN (POS Z) (ADD1 (NEG Z)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS X) (ADD1 (NEG Z)))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Y Z
(ZN (POS Z) (ADD1 (NEG Z)))))),
which again simplifies, unfolding the definitions of ZLESSEQP,
ZLESSP, and TAK0, to:
T.
Case 12.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z (TAK0 Z X X))).
But this simplifies again, using linear arithmetic, to:
T.
Case 11.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
X X))).
But this simplifies again, rewriting with POS-ZN and NEG-ZN, and
expanding the functions ZLESSEQP, ZLESSP, and TAK0, to:
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (ADD1 (NEG X)))
(PLUS (NEG X) (POS X)))
(LESSP (PLUS (POS X) (NEG X))
(PLUS (NEG X) (POS X))))
(EQUAL X
(ZN (POS X) (ADD1 (NEG X))))),
which we again simplify, using linear arithmetic, to:
T.
Case 10.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X (TAK0 Y X X))),
which again simplifies, expanding the definitions of ZLESSEQP,
ZLESSP, and TAK0, to the new conjecture:
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Y))
(PLUS (NEG X) (POS Y)))
(LESSP (PLUS (POS X) (NEG X))
(PLUS (NEG X) (POS X))))
(EQUAL X Y)),
which again simplifies, using linear arithmetic, to:
T.
Case 9. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z (TAK0 Y X X))),
which again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Z
(ZN (POS Y) (ADD1 (NEG Y)))
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
(ZN (POS Y) (ADD1 (NEG Y)))
X))),
which we again simplify, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 Y
(ZN (POS Y) (ADD1 (NEG Y)))
X))).
This simplifies again, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
(LESSP (PLUS (POS Z) (ADD1 (NEG Y)))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z)))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z
(TAK0 Y
(ZN (POS Y) (ADD1 (NEG Y)))
X))),
which we again simplify, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z (TAK0 Z Z X))),
which we again simplify, opening up the functions ZLESSEQP, ZLESSP,
and TAK0, to:
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y)))
(LESSP (PLUS (POS Z) (NEG Z))
(PLUS (NEG Z) (POS Z)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (NEG Z))))
(EQUAL Z X)),
which we again simplify, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X
(TAK0 (ZN (POS X) (ADD1 (NEG X)))
Z X))),
which we again simplify, appealing to the lemmas POS-ZN and NEG-ZN,
and unfolding the functions ZLESSEQP, ZLESSP, and TAK0, to the
following two new goals:
Case 3.2.
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y)))
( LEQ
(PLUS (NEG Z) (POS X))
(PLUS (POS Z) (ADD1 (NEG X)))))
(EQUAL X Z)).
But this simplifies again, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
(LESSP (PLUS (POS Y) (ADD1 (NEG X)))
(PLUS (NEG Y) (POS X)))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS Z) (ADD1 (NEG X)))
(PLUS (NEG Z) (POS X)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z))))
(EQUAL X
(ZN (POS X) (ADD1 (NEG X))))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y))))
(EQUAL X (TAK0 Y Z X))).
This simplifies again, unfolding the definitions of ZLESSEQP,
ZLESSP, and TAK0, to the new conjecture:
(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
(LESSP (PLUS (POS Z) (NEG Y))
(PLUS (NEG Z) (POS Y)))
(LESSP (PLUS (POS X) (NEG Z))
(PLUS (NEG X) (POS Z))))
(EQUAL X Y)),
which we again simplify, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X))
(PLUS (NEG Y) (POS X)))
( LEQ
(PLUS (NEG X) (POS Z))
(PLUS (POS X) (ADD1 (NEG Z))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (ADD1 (NEG Y))))
( LEQ
(PLUS (NEG Y) (POS X))
(PLUS (POS Y) (ADD1 (NEG X))))
( LEQ
(PLUS (NEG Z) (POS Y))
(PLUS (POS Z) (NEG Y))))
(EQUAL Z (TAK0 Y Z X))).
But this simplifies again, opening up ZLESSEQP, ZLESSP, and TAK0,
to:
T.
Q.E.D.
[ 8.1930003 2.4849996 ]
TAK0-SATISFIES-TAK-EQUATION
(r '(REVERSE '(A B C)))
(QUOTE (C B A))
(r '(FLATTEN '((A . B) . (C . D))))
(QUOTE (A B C D))
(r '(MC-FLATTEN '((A . B) . (C . D)) NIL))
(QUOTE (A B C D))
(r '(ZN 0 1))
(ZN 0. 1.)
(r '(POS (ZN 0 1)))
0.
(r '(NEG (ZN 0 1)))
1.
(r '(ZNP (ZN 0 1)))
T
(DEFN ZNORM (X)
(IF (LESSP (POS X) (NEG X))
(ZN 0 (DIFFERENCE (NEG X) (POS X)))
(ZN (DIFFERENCE (POS X) (NEG X)) 0)))
Note that (ZNP (ZNORM X)) is a theorem.
[ 0.61100006 0.0100001018 ]
ZNORM
(setq no-built-in-arith-flg t)
(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE)
(EQUAL (PLUS X (PLUS Y Z))
(PLUS Y (PLUS X Z))))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X)))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
(EQUAL (PLUS X Y)
(PLUS Y X)))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest two inductions, both of which are flawed. We
limit our consideration to the two suggested by the largest number of
nonprimitive recursive functions in the conjecture. Since both of
these are equally likely, we will choose arbitrarily. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP X) (P X Y))
(IMPLIES (AND (NOT (ZEROP X)) (P (SUB1 X) Y))
(P X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces two new formulas:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (PLUS X Y) (PLUS Y X))).
This simplifies, opening up the definitions of ZEROP, EQUAL, and
PLUS, to four new conjectures:
Case 2.4.
(IMPLIES (AND (EQUAL X 0) (NOT (NUMBERP Y)))
(EQUAL 0 (PLUS Y 0))),
which again simplifies, unfolding the functions NUMBERP, PLUS,
and EQUAL, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL X 0) (NUMBERP Y))
(EQUAL Y (PLUS Y 0))).
This again simplifies, trivially, to the new conjecture:
(IMPLIES (NUMBERP Y)
(EQUAL Y (PLUS Y 0))),
which we will name *1.1.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP X))
(NOT (NUMBERP Y)))
(EQUAL 0 (PLUS Y X))),
which we again simplify, opening up PLUS and EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP X)) (NUMBERP Y))
(EQUAL Y (PLUS Y X))),
which we will name *1.2.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (PLUS (SUB1 X) Y)
(PLUS Y (SUB1 X))))
(EQUAL (PLUS X Y) (PLUS Y X))).
This simplifies, expanding the functions ZEROP and PLUS, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (PLUS (SUB1 X) Y)
(PLUS Y (SUB1 X))))
(EQUAL (ADD1 (PLUS Y (SUB1 X)))
(PLUS Y X))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate
(SUB1 X). We rely upon the type restriction lemma noted when SUB1
was introduced to restrict the new variable. This produces:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (PLUS Z Y) (PLUS Y Z)))
(EQUAL (ADD1 (PLUS Y Z))
(PLUS Y (ADD1 Z)))).
Of course, this simplifies further, clearly, to the new formula:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (PLUS Z Y) (PLUS Y Z)))
(EQUAL (ADD1 (PLUS Y Z))
(PLUS Y (ADD1 Z)))).
We use the above equality hypothesis by substituting (PLUS Z Y) for
(PLUS Y Z) and throwing away the equality. We thus obtain:
(IMPLIES (NUMBERP Z)
(EQUAL (ADD1 (PLUS Z Y))
(PLUS Y (ADD1 Z)))),
which we will name *1.3.
We will try to prove it by induction. There are two plausible
inductions. However, only one is unflawed. We will induct according
to the following scheme:
(AND (IMPLIES (ZEROP Z) (P Z Y))
(IMPLIES (AND (NOT (ZEROP Z)) (P (SUB1 Z) Y))
(P Z Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP can be used to show that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates
the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Z) (NUMBERP Z))
(EQUAL (ADD1 (PLUS Z Y))
(PLUS Y (ADD1 Z)))).
This simplifies, opening up the definitions of ZEROP, NUMBERP,
EQUAL, PLUS, and ADD1, to the following two new goals:
Case 2.2.
(IMPLIES (AND (EQUAL Z 0) (NOT (NUMBERP Y)))
(EQUAL 1 (PLUS Y 1))).
This simplifies again, opening up the definitions of NUMBERP,
PLUS, and EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL Z 0) (NUMBERP Y))
(EQUAL (ADD1 Y) (PLUS Y 1))),
which we again simplify, clearly, to the new goal:
(IMPLIES (NUMBERP Y)
(EQUAL (ADD1 Y) (PLUS Y 1))),
which we will name *1.3.1.
Case 1. (IMPLIES (AND (NOT (ZEROP Z))
(EQUAL (ADD1 (PLUS (SUB1 Z) Y))
(PLUS Y (ADD1 (SUB1 Z))))
(NUMBERP Z))
(EQUAL (ADD1 (PLUS Z Y))
(PLUS Y (ADD1 Z)))),
which we simplify, applying ADD1-SUB1, and expanding ZEROP and PLUS,
to the formula:
(IMPLIES (AND (NOT (EQUAL Z 0))
(EQUAL (ADD1 (PLUS (SUB1 Z) Y))
(PLUS Y Z))
(NUMBERP Z))
(EQUAL (ADD1 (PLUS Y Z))
(PLUS Y (ADD1 Z)))).
Appealing to the lemma SUB1-ELIM, replace Z by (ADD1 X) to
eliminate (SUB1 Z). We use the type restriction lemma noted when
SUB1 was introduced to restrict the new variable. We thus obtain:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(EQUAL (ADD1 (PLUS X Y))
(PLUS Y (ADD1 X))))
(EQUAL (ADD1 (PLUS Y (ADD1 X)))
(PLUS Y (ADD1 (ADD1 X))))).
Of course, this further simplifies, clearly, to:
(IMPLIES (AND (NUMBERP X)
(EQUAL (ADD1 (PLUS X Y))
(PLUS Y (ADD1 X))))
(EQUAL (ADD1 (ADD1 (PLUS X Y)))
(PLUS Y (ADD1 (ADD1 X))))).
We use the above equality hypothesis by substituting
(PLUS Y (ADD1 X)) for (ADD1 (PLUS X Y)) and throwing away the
equality. We must thus prove:
(IMPLIES (NUMBERP X)
(EQUAL (ADD1 (PLUS Y (ADD1 X)))
(PLUS Y (ADD1 (ADD1 X))))).
Name the above subgoal *1.3.2.
We will try to prove it by induction. There are two plausible
inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (ZEROP Y) (P Y X))
(IMPLIES (AND (NOT (ZEROP Y)) (P (SUB1 Y) X))
(P Y X))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP establish that the measure (COUNT Y) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following
two new goals:
Case 2. (IMPLIES (AND (ZEROP Y) (NUMBERP X))
(EQUAL (ADD1 (PLUS Y (ADD1 X)))
(PLUS Y (ADD1 (ADD1 X))))).
This simplifies, expanding the definitions of ZEROP, EQUAL, and
PLUS, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(EQUAL (ADD1 (PLUS (SUB1 Y) (ADD1 X)))
(PLUS (SUB1 Y) (ADD1 (ADD1 X))))
(NUMBERP X))
(EQUAL (ADD1 (PLUS Y (ADD1 X)))
(PLUS Y (ADD1 (ADD1 X))))),
which simplifies, expanding the functions ZEROP and PLUS, to:
T.
That finishes the proof of *1.3.2.
So next consider:
(IMPLIES (NUMBERP Y)
(EQUAL (ADD1 Y) (PLUS Y 1))),
which is formula *1.3.1 above. Let us appeal to the induction
principle. There is only one suggested induction. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP Y) (P Y))
(IMPLIES (AND (NOT (ZEROP Y)) (P (SUB1 Y)))
(P Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP can be used to establish that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Y) (NUMBERP Y))
(EQUAL (ADD1 Y) (PLUS Y 1))).
This simplifies, opening up the functions ZEROP, NUMBERP, ADD1,
PLUS, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(EQUAL (ADD1 (SUB1 Y))
(PLUS (SUB1 Y) 1))
(NUMBERP Y))
(EQUAL (ADD1 Y) (PLUS Y 1))),
which simplifies, rewriting with ADD1-SUB1, and opening up the
functions ZEROP and PLUS, to:
T.
That finishes the proof of *1.3.1, which, consequently, finishes
the proof of *1.3.
So let us turn our attention to:
(IMPLIES (AND (NOT (NUMBERP X)) (NUMBERP Y))
(EQUAL Y (PLUS Y X))),
which we named *1.2 above. We will try to prove it by induction.
There is only one plausible induction. We will induct according to
the following scheme:
(AND (IMPLIES (ZEROP Y) (P Y X))
(IMPLIES (AND (NOT (ZEROP Y)) (P (SUB1 Y) X))
(P Y X))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP can be used to establish that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates two new formulas:
Case 2. (IMPLIES (AND (ZEROP Y)
(NOT (NUMBERP X))
(NUMBERP Y))
(EQUAL Y (PLUS Y X))),
which simplifies, unfolding the functions ZEROP, NUMBERP, EQUAL,
and PLUS, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(EQUAL (SUB1 Y) (PLUS (SUB1 Y) X))
(NOT (NUMBERP X))
(NUMBERP Y))
(EQUAL Y (PLUS Y X))).
This simplifies, applying ADD1-SUB1, and unfolding the definitions
of ZEROP and PLUS, to:
T.
That finishes the proof of *1.2.
So we now return to:
(IMPLIES (NUMBERP Y)
(EQUAL Y (PLUS Y 0))),
which we named *1.1 above. Perhaps we can prove it by induction.
There is only one suggested induction. We will induct according to
the following scheme:
(AND (IMPLIES (ZEROP Y) (P Y))
(IMPLIES (AND (NOT (ZEROP Y)) (P (SUB1 Y)))
(P Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definition of ZEROP can be used to prove that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme produces
the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Y) (NUMBERP Y))
(EQUAL Y (PLUS Y 0))).
This simplifies, expanding ZEROP, NUMBERP, PLUS, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(EQUAL (SUB1 Y) (PLUS (SUB1 Y) 0))
(NUMBERP Y))
(EQUAL Y (PLUS Y 0))).
This simplifies, appealing to the lemma ADD1-SUB1, and opening up
ZEROP and PLUS, to:
T.
That finishes the proof of *1.1, which also finishes the proof
of *1. Q.E.D.
[ 3.17299995 1.72000007 ]
COMMUTATIVITY-OF-PLUS